k(v:B) sends
kf(x:A,v) on
kl tagged with tg:T
kprovided c(x,v)
== ((vartype(source(l);x) r A)
== & (e:E. (loc(e) = source(l))  (kind(e) = k)  (valtype(e) r B))
== & (e:E. (kind(e) = rcv(l,tg))  (valtype(e) r T)))
== c (e:E.
== c (loc(e) = source(l))
== c  (kind(e) = k)
== c  ((((c((x when e),val(e))))
== c  (( (e':E
== c  (( (((kind(e') = rcv(l,tg))
== c  (( (c (sender(e') = e
== c  (( (c & (e'':E. (kind(e'') = rcv(l,tg))  (sender(e'') = e)  (e'' = e'))
== c  (( (c & val(e') = f((x when e),val(e))))))
== c  & ((((c((x when e),val(e)))))
== c  & ( ((e':E. ((kind(e') = rcv(l,tg)) c (sender(e') = e))))))) 

latex

---

clarification:

conditional-send1-p(es;x;A;k;B;l;tg;T;c;f)
== ((es-vartype(es; source(l); x) r A)
== & (e:es-E(es).
== & ((es-loc(es; e) = source(l)  Id)  (es-kind(es; e) = k  Knd)  (es-valtype(es; e) r B))
== & (e:es-E(es). (es-kind(es; e) = rcv(l,tg)  Knd)  (es-valtype(es; e) r T)))
== c (e:es-E(es).
== c (es-loc(es; e) = source(l)  Id)
== c  (es-kind(es; e) = k  Knd)
== c  ((((c(es-when(es; x; e),es-val(es; e))))
== c  (( (e':es-E(es)
== c  (( (((es-kind(es; e') = rcv(l,tg)  Knd)
== c  (( (c (es-sender(es; e') = e  es-E(es)
== c  (( (c & (e'':es-E(es).
== c  (( (c & ((es-kind(es; e'') = rcv(l,tg)  Knd)
== c  (( (c & ( (es-sender(es; e'') = e  es-E(es))
== c  (( (c & ( (e'' = e'  es-E(es)))
== c  (( (c & es-val(es; e') = f(es-when(es; x; e),es-val(es; e))  T))))
== c  & ((((c(es-when(es; x; e),es-val(es; e)))))
== c  & ( ((e':es-E(es)
== c  & ( ((((es-kind(es; e') = rcv(l,tg)  Knd)
== c  & ( ((c (es-sender(es; e') = e  es-E(es)))))))) 

latex

Definitions	vartype(i;x), valtype(e), Id, loc(e), source(l), P & Q, x:A. B(x), P  Q, b, f(a), x when e, val(e), A, x:A. B(x), A c B, Knd, kind(e), rcv(l,tg), s = t, E, sender(e)
FDL editor aliases	conditional-send1-p